(* 作业1 *)

(* 引理 imp_perm *)
(* 该引理的含义是：如果我们知道 (P -> Q -> R)，那么可以推导出 (Q -> P -> R)，
   即蕴含的顺序可以交换。 *)
Lemma imp_perm: forall P Q R: Prop, (P -> Q -> R) -> (Q -> P -> R).
Proof.
  intros P Q R H q p. (* 假设 P、Q、R 是命题，H 是 (P -> Q -> R)，q 是 Q，p 是 P。 *)
  apply H; assumption. (* 使用 H，分别对 P 和 Q 应用假设 q 和 p。 *)
Qed.

(* 引理 delta_impR *)
(* 该引理的含义是：如果我们知道 (P -> Q)，那么可以推导出 (P -> P -> Q)，
   即重复的 P 不会改变结论。 *)
Lemma delta_impR: forall P Q: Prop, (P -> Q) -> (P -> P -> Q).
Proof.
  intros P Q H p1 p2. (* 假设 P 和 Q 是命题，H 是 (P -> Q)，p1 和 p2 是 P。 *)
  apply H; assumption. (* 使用 H 和假设 p1，得出 Q。 *)
Qed.

(* 引理 diamond *)
(* 该引理的含义是：如果我们有以下假设：
   1. (P -> Q)
   2. (P -> R)
   3. (Q -> R -> T)
   那么可以从 P 推导出 T。 *)
Lemma diamond: forall P Q R T: Prop, (P -> Q) -> (P -> R) -> (Q -> R -> T) -> P -> T.
Proof.
  intros P Q R T H1 H2 H3 p. (* 假设 P、Q、R、T 是命题，H1 是 (P -> Q)，H2 是 (P -> R)，H3 是 (Q -> R -> T)，p 是 P。 *)
  apply H3. (* 使用 H3，我们需要证明 Q 和 R。 *)
  - apply H1; assumption. (* 使用 H1 和假设 p，得出 Q。 *)
  - apply H2; assumption. (* 使用 H2 和假设 p，得出 R。 *)
Qed.

(* 引理 weak_peirce *)
(* 该引理的含义是弱化的皮尔士定律：
   如果 (((P -> Q) -> P) -> P) -> Q 成立，那么 Q 必然成立。 *)
Lemma weak_peirce: forall P Q: Prop, ((((P -> Q) -> P) -> P) -> Q) -> Q.
Proof.
  intros P Q H. (* 假设 P 和 Q 是命题，H 是 ((((P -> Q) -> P) -> P) -> Q)。 *)
  apply H. (* 使用 H，我们需要证明 (((P -> Q) -> P) -> P)。 *)
  intros H1. (* 假设 H1 是 ((P -> Q) -> P)。 *)
  apply H1. (* 使用 H1，我们需要证明 (P -> Q)。 *)
  intros H2. (* 假设 H2 是 P。 *)
  apply H. (* 再次使用 H，我们需要证明 (((P -> Q) -> P) -> P)。 *)
  intros H3. (* 假设 H3 是 ((P -> Q) -> P)。 *)
  exact H2. (* 使用假设 H2，我们完成证明。 *)
Qed.




(* 作业2 *)

(* 定理 all_perm *)
(* 该定理的含义是：如果对于任意 x 和 y，P x y 成立，那么对于任意 x 和 y，P y x 也成立。
   换句话说，命题 P 对于所有参数的顺序是对称的。 *)
Theorem all_perm:
    forall (A : Type) (P : A -> A -> Prop),
    (forall x y : A, P x y) ->
    forall x y : A, P y x.
Proof.
  intros A P H x y. (* 假设 A 是一个类型，P 是 A -> A -> Prop 类型的命题，H 是 (forall x y : A, P x y)，x 和 y 是 A 的元素。 *)
  apply H. (* 使用 H：因为 H 声明了对于任意 x 和 y，P x y 成立，所以直接应用即可。 *)
Qed.

(* 定理 resolution *)
(* 该定理的含义是：如果我们有以下假设：
   1. (forall a : A, Q a -> R a -> S a) （对于任意 a，Q a 和 R a 蕴含 S a），
   2. (forall b : A, P b -> Q b) （对于任意 b，P b 蕴含 Q b），
   那么我们可以推导出：
   (forall c : A, P c -> R c -> S c) （对于任意 c，P c 和 R c 蕴含 S c）。 *)
Theorem resolution:
    forall (A : Type) (P Q R S : A -> Prop),
       (forall a : A, Q a -> R a -> S a) -> (* 假设 1：Q 和 R 蕴含 S *)
       (forall b : A, P b -> Q b) ->        (* 假设 2：P 蕴含 Q *)
       (forall c : A, P c -> R c -> S c).   (* 目标：P 和 R 蕴含 S *)
Proof.
  intros A P Q R S H1 H2 c Pc Rc. (* 假设 A 是一个类型，P、Q、R、S 是 A -> Prop 类型的命题，H1 和 H2 是前提，c 是 A 的一个元素，Pc 和 Rc 是 P c 和 R c 的假设。 *)
  apply H1. (* 使用 H1：我们需要证明 Q c 和 R c。 *)
  - apply H2. (* 使用 H2：因为 H2 声明了 P c 蕴含 Q c，所以我们需要证明 P c。 *)
    assumption. (* 假设 Pc 已经成立，直接使用即可。 *)
  - assumption. (* 假设 Rc 已经成立，直接使用即可。 *)
Qed.




(* 作业3 *)

(* 引理 nf *)
(* 该引理的含义是：逻辑上 False 是不可能成立的，即 ~False。 *)
Lemma nf: ~False.
Proof.
  unfold not. (* 展开 ~False 的定义，即 False -> False。 *)
  intros H. (* 假设 H 是 False，我们需要从 H 推导出 False。 *)
  assumption. (* H 本身就是 False，所以直接使用 H 即可完成证明。 *)
Qed.

(* 引理 nnnp *)
(* 该引理的含义是：对于任意命题 P，如果 ~~~P 成立，那么 ~P 也成立。
   换句话说，三重否定蕴含单重否定。 *)
Lemma nnnp: forall P: Prop, ~~~P -> ~P.
Proof.
  unfold not. (* 展开 ~~~P 和 ~P 的定义：~~~P = (P -> False) -> False，~P = P -> False。 *)
  intros P H H1. (* 假设 P 是一个命题，H 是 ~~~P，H1 是 P。 *)
  apply H. (* 使用 H，我们需要证明 P -> False。 *)
  intros H2. (* 假设 H2 是 P。 *)
  apply H2. (* 使用 H2，我们需要证明 False。 *)
  assumption. (* 假设 H1 是 P，因此直接使用 H1 即可完成证明。 *)
Qed.

(* 引理 nnnpp *)
(* 该引理的含义是：对于任意命题 P 和 Q，如果 ~~~P 成立并且 P 成立，那么可以推出 Q。
   这是因为 ~~~P 和 P 的组合会导致矛盾，从而可以推出任何命题 Q。 *)
Lemma nnnpp: forall P Q: Prop, ~~~P -> P -> Q.
Proof.
  unfold not. (* 展开 ~~~P 的定义：~~~P = (P -> False) -> False。 *)
  intros P Q H H1. (* 假设 P 和 Q 是命题，H 是 ~~~P，H1 是 P。 *)
  exfalso. (* 使用 `exfalso` 策略，目标变为证明 False。 *)
  apply H. (* 使用 H，我们需要证明 P -> False。 *)
  intros H2. (* 假设 H2 是 P。 *)
  apply H2. (* 使用 H2，我们需要证明 False。 *)
  assumption. (* 假设 H1 是 P，因此直接使用 H1 即可完成证明。 *)
Qed.

(* 引理 pqnq *)
(* 该引理的含义是：如果 P -> Q 且 ~Q，那么可以推出 ~P。
   换句话说，如果 P 蕴含 Q，而 Q 不成立，那么 P 也不可能成立。 *)
Lemma pqnq: forall P Q: Prop, (P -> Q) -> ~Q -> ~P.
Proof.
  unfold not. (* 展开 ~Q 和 ~P 的定义：~Q = Q -> False，~P = P -> False。 *)
  intros P Q H H1 H2. (* 假设 P 和 Q 是命题，H 是 P -> Q，H1 是 ~Q，H2 是 P。 *)
  apply H1. (* 使用 H1，我们需要证明 Q。 *)
  apply H. (* 使用 H，我们需要证明 Q。 *)
  assumption. (* 假设 H2 是 P，因此直接使用 H2 即可完成证明。 *)
Qed.

(* 引理 pqrpq *)
(* 该引理的含义是：如果 P -> Q 且 P -> ~Q，那么 P 成立时可以推出任何命题 R。
   这是因为 P -> Q 和 P -> ~Q 的组合会导致矛盾，从而可以推出任何命题。 *)
Lemma pqrpq: forall P Q R: Prop, (P -> Q) -> (P -> ~Q) -> P -> R.
Proof.
  unfold not. (* 展开 ~Q 的定义：~Q = Q -> False。 *)
  intros P Q R H H1 H2. (* 假设 P、Q 和 R 是命题，H 是 P -> Q，H1 是 P -> ~Q，H2 是 P。 *)
  exfalso. (* 使用 `exfalso` 策略，目标变为证明 False。 *)
  apply (H1 H2). (* 使用 H1 和假设 H2，我们需要证明 Q。 *)
  apply (H H2). (* 使用 H 和假设 H2，我们得出 Q，从而完成证明。 *)
Qed.



(* 作业4 *)
(* 引理 and4 *)
Lemma and4: forall (A: Set) (a b c d: A),
  a = c \/ b = c \/ c = c \/ d = c.
Proof.
  intros A a b c d.
  (* 使用等式的自反性 *)
  right. (* 选择 c = c *)
  right. (* 选择 d = c *)
  left. (* 选择 c = c *)
  reflexivity. (* 证明 c = c *)
Qed.


(* 引理 and_asso *)
Lemma and_asso: forall A B C: Prop,
  A /\ (B /\ C) -> (A /\ B) /\ C.
Proof.
  intros A B C H.
  destruct H as [HA [HB HC]]. (* 分解合取 *)
  split. (* 证明 (A /\ B) *)
  split. (* 进一步分解 (A /\ B) *)
  exact HA. (* 使用 HA *)
  exact HB. (* 使用 HB *)
  exact HC. (* 使用 HC 证明 C *)
Qed.


(* 引理 and_abcd *)
Lemma and_abcd: forall A B C D: Prop,
  (A -> B) /\ (C -> D) /\ A /\ C -> B /\ D.
Proof.
  intros A B C D H.
  destruct H as [H1 [H2 [H3 H4]]]. (* 分解合取 *)
  apply H1 in H3. (* 使用 A -> B *)
  apply H2 in H4. (* 使用 C -> D *)
  split. (* 证明 B /\ D *)
  exact H3. (* 使用 H3 证明 B *)
  exact H4. (* 使用 H4 证明 D *)
Qed.


(* 引理 nana *)
Lemma nana: forall A: Prop, ~(A /\ ~A).
Proof.
  unfold not.
  intros A H.
  destruct H as [H1 H2]. (* 分解合取 *)
  apply H2 in H1. (* 使用 ~A *)
  assumption. (* 得到矛盾 *)
Qed.


(* 引理 or_asso *)
Lemma or_asso: forall A B C: Prop,
  A \/ (B \/ C) -> (A \/ B) \/ C.
Proof.
  intros A B C H.
  destruct H as [H1 | H2].
  - (* 处理 A 的情况 *)
    left. left. exact H1.
  - (* 处理 B \/ C 的情况 *)
    destruct H2 as [H3 | H4].
    + (* 处理 B 的情况 *)
      left. right. exact H3.
    + (* 处理 C 的情况 *)
      right. exact H4.
Qed.


(* 引理 abna *)
Lemma abna: forall A B: Prop, (A \/ B) /\ ~A -> B.
Proof.
  intros A B H.
  destruct H as [H1 H2]. (* 分解合取 *)
  destruct H1 as [H3 | H4]. (* 分解析取 *)
  exfalso. (* 引入矛盾证明 *)
  apply H2 in H3. (* 使用 H2 和 H3 得到矛盾 *)
  exact H3. (* 矛盾证明完成 *)
  exact H4. (* 如果 B 为真，直接返回 B *)
Qed.


Require Import Coq.Logic.Classical. (* 引入经典逻辑 *)

(* 引理 nnana *)
Lemma nnana: forall A: Prop, ~~(A \/ ~A).
Proof.
  intros A H.
  (* 使用 assert 引入排中律 *)
  assert (H1: A \/ ~A).
  {
    apply classic. (* 使用经典逻辑中的排中律 *)
  }
  apply H in H1. (* 使用假设 H: ~~(A \/ ~A) *)
  assumption. (* 得到矛盾，完成证明 *)
Qed.



(* 作业5 *)
Section Proofs.

(* 假设 A 是一个集合，P 和 Q 是 A -> Prop 类型的命题 *)
Variable A : Set.
Variable P Q : A -> Prop.

(* 引理 ex1 *)
Lemma ex1: (exists x: A, P x \/ Q x) -> (exists x: A, P x) \/ (exists x: A, Q x).
Proof.
  intros H. (* 假设 H: 存在 x 使得 P x \/ Q x *)
  destruct H as [x Hx]. (* 解构存在性，得到 x 和 Hx: P x \/ Q x *)
  destruct Hx as [HP | HQ]. (* 解构析取 Hx: P x 或 Q x *)
  - left. (* 如果 P x 成立，则左侧成立 *)
    exists x. (* 构造存在性 *)
    exact HP. (* 提供证明 P x 成立 *)
  - right. (* 如果 Q x 成立，则右侧成立 *)
    exists x. (* 构造存在性 *)
    exact HQ. (* 提供证明 Q x 成立 *)
Qed.


(* 引理 ex2 *)
Lemma ex2: (exists x: A, P x) \/ (exists x: A, Q x) -> exists x: A, P x \/ Q x.
Proof.
  intros H. (* 假设 H: (exists x: A, P x) \/ (exists x: A, Q x) *)
  destruct H as [HP | HQ]. (* 解构析取 H: 存在性 P 或 存在性 Q *)
  - destruct HP as [x Px]. (* 解构存在性 P *)
    exists x. (* 构造存在性 *)
    left. (* 构造析取左侧 *)
    exact Px. (* 提供证明 P x 成立 *)
  - destruct HQ as [x Qx]. (* 解构存在性 Q *)
    exists x. (* 构造存在性 *)
    right. (* 构造析取右侧 *)
    exact Qx. (* 提供证明 Q x 成立 *)
Qed.



(* 引理 ex3 *)
Lemma ex3: (forall x: A, P x) -> ~(exists y: A, ~ P y).
Proof.
  intros H HP. (* 假设 H: 对所有 x 有 P x，且假设 HP: 存在 y 使得 ~ P y *)
  destruct HP as [y Hy]. (* 解构存在性 HP，得到 y 和 Hy: ~ P y *)
  apply Hy. (* 使用 Hy: ~ P y *)
  apply H. (* 使用 H: 对所有 x 有 P x *)
Qed.


(* 引理 ex4 *)
Lemma ex4: (exists x: A, forall R: A -> Prop, R x) -> 2 = 3.
Proof.
  intros H. (* 假设 H: 存在 x 使得对所有 R: A -> Prop, R x *)
  destruct H as [x Hx]. (* 解构存在性 H，得到 x 和 Hx: forall R, R x *)
  assert (False). (* 我们需要证明 False *)
  {
    specialize (Hx (fun _ => False)). (* 令 R 为 False *)
    exact Hx. (* 使用 Hx: R x，即 False 成立，得到矛盾 *)
  }
  contradiction. (* 使用 False 推出矛盾，完成证明 *)
Qed.

End Proofs.



(* 打印所有证明的结果以验证 *)
Print imp_perm.
Print delta_impR.
Print diamond.
Print weak_peirce.
Print all_perm.
Print resolution.
Print nf.
Print nnnp.
Print nnnpp.
Print pqnq.
Print pqrpq.
Print and4.
Print and_asso.
Print and_abcd.
Print nana.
Print or_asso.
Print abna.
Print nnana.
Print ex1.
Print ex2.
Print ex3.
Print ex4.
